A:Type, f,g:fpf(A; a.top), eq:EqDecider(A), x:A.
(x  fpf-domain(fpf-join(eq; f; g)))  ((x  fpf-domain(f))  (x  fpf-domain(g))) 

latex

Definitions	t  T, top, x.A(x), x:A. B(x), x. t(x), P  Q, P  Q, P  Q, P  Q, Type, fpf(A; a.B(a)), EqDecider(T), fpf-join(eq; f; g), fpf-dom(eq; x; f), b, guard(T), P  Q, x:AB(x), left + right, fpf-domain(f), (x  l), prop{i:l}, x:A  B(x)
Lemmas	iff functionality wrt iff, fpf-join-dom, l member wf, fpf-domain wf, assert wf, fpf-dom wf, deq wf, fpf wf, member-fpf-domain, fpf-join wf, top wf